T:Type, P, Q:((T List)Prop), L:T List.
star-append(T;P;Q)(L)

Q(L)  (L1, L2:T List. L = (L1 @ L2) & P(L1) & star-append(T;P;Q)(L2)) 

latex

Definitions	P & Q, x:A. B(x), t  T, Prop, x:A. B(x), concat(ll), as @ bs, x. t(x), xL. P(x), P  Q, P  Q, P  Q, P  Q, star-append(T;P;Q), {T}
Lemmas	l all nil, append assoc, l all cons, l all wf, append wf, concat wf